# PRZEMEK
Sprawdzacz dowodów matematycznych implementujący teorię typów Per Martin-Löf'a
https://en.wikipedia.org/wiki/Intuitionistic_type_theory

```sbt
> $ sbt run 
Dzień dobry
Aktualnie zajmuje się sprawdzaniem typów.
Podaj coś to ci powiem jaki ma typ
np. polimorficza funkcja identycznościowa
(lambda (A (Universe 0)) (lambda (x A) x))
albo użyta do tyou jednostkowego
((lambda (A (Universe 0)) (lambda (x A) x)) Unit)
a potem zaaplikowana do przedstawiciela typu jednostkowego
(((lambda (A (Universe 0)) (lambda (x A) x)) Unit) tt)
Fajne co nie?
Inna opcja to wczytanie pliku z kodem
-f example.prmk

> $ sbt 'run -f example.prmk'
Kod: ((lambda (A (universe 0)) (lambda (x A) x)) unit)
Przed Bruinizacją: PiElim(PiValue(NamedType(A,Universe(0)),PiValue(NamedType(x,Var(A)),Var(x))),UnitType)
Ads: PiElim(PiValue(Universe(0),PiValue(Bruijn(0),Bruijn(0))),UnitType)
Znormalizowane: PiValue(UnitType,Bruijn(0))
Typ: PiType(UnitType,UnitType)
```

## Zajawka
W pliku `Nat.prmk` można zobaczyć jak wygląda definicja liczb naturalnych, zera, następnika i mnożenia przez 2 gdy są zakodowane jako W-typ

## Kompilacja
```
sbt package
```
Można odwrócić zmianę `fc4256ce8a633254ea35b794ef41f2c07173d80f` i kompilować rodzimo (przez Scala Native; porzuciłem to bo kod wynikowy jest wolny)
```
sbt 'set nativeMode := "release"' compile nativeLink
target/scala-2.11/przemek-out -f example.prmk 

```

## Do zrobienia
 * ~~wszechświaty~~ ✓ 
 * ~~Pi-typy~~ ✓
 * ~~Typy identycznościowe~~ ✓
 * ~~Sigma-typy~~ ✓
 * ~~Sumowane typy~~ ✓ 
 * ~~W-typy~~ ✓
 * ~~nazwane zmienne (żeby nie trzeba było DeBruijnami)~~ ✓
 * ~~Deklarowanie stałych~~ ✓ 
 * strukturalna rekurencja
 * ogarnięte błędy kompilacji
 * ładne wypisywanie wyników
 * biblioteka twierdzeń (Eckmann-Hilton na początek)
 * Polimorficzność wszechświatów
 * Naprawienie błędów powstałych przy tworzeniu powyższego
 * Makra lispowe xD
 * Optymalizacja (pamięć znormalizowanych/sprawdzonych wyrażeń?)
